COMMENT ⊗   VALID 00008 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	%ysp[w88,jmc]		Another attack on the Yale shooting problem
C00003 00003	Propositional version
C00004 00004	Quantified version
C00006 00005	Situation calculus version (with minimal other quantification)
C00008 00006	persistent p ∧ holds(p,t) ∧ (∀e)(causes(e,not p,t) ⊃ ¬occurs(e,t)) ⊃ holds(p,t+1)
C00009 00007	(∀p t)(holds(p,t) ∧ (∀e)(causes(e,not p,t) ⊃ ¬occurs(e,t)) ⊃ holds(p,t+1))
C00011 00008	∂29-Mar-88  1324	VAL 	re: YSP   
C00012 ENDMK
C⊗;
%ysp[w88,jmc]		Another attack on the Yale shooting problem
Old version with unintended models

holds(p,s) ∧ persistent p ∧ ¬ab1(p,e,s) ⊃ holds(p,r(e,s))

persistent alive
persistent loaded

holds(loaded,r(load,s))
holds(loaded,s) ⊃ ¬holds(alive,r(shoot,s))

holds(alive,S0)

Propositional version

¬ul* ∧ ul ⊃ ab1
ul* ⊃ ul

¬shoot* ∧ shoot ⊃ ab2
shoot* ⊃ shoot

¬heartattack* ∧ heartattack ⊃ ab3
heartattack* ⊃ heartattack

¬ul*
shoot*
¬heartattack*

shoot ∧ ¬ul ∧ ¬ab4 ⊃ ¬alive ∧ ¬ab17

heartattack ∧ ¬ab5 ⊃ ¬alive ∧ ¬ab17

¬ab17 ∧ ¬shoot ∧ ¬heartattack ⊃ alive


Quantified version

∀prop.¬asserted prop ∧ holds prop ⊃ ab(prop)
∀prop.asserted prop ⊃ holds prop

¬asserted ul
asserted shoot
¬asserted heartattack

holds heartattack ∧ ¬ab6 ⊃ fatalheartattack

holds shoot  ∧ ¬holds ul ⊃ shotfred

killfred shotfred
killfred fatalheartattack
¬killfred unload

∀prop.[killfred prop ∧ holds prop ∧ ¬ab1(prop) ⊃ ¬alive ∧ ¬ab17]

¬ab17 ∧ [∀prop.killfred prop ⊃ ¬holds prop] ⊃ alive


Situation calculus version (with minimal other quantification)

∀prop.¬asserted prop ∧ holds prop ⊃ ab(prop)
∀prop.asserted prop ⊃ holds prop
These two axioms are just as in the non situation calculus version.

∀s.¬asserted occurs(unload,s)
∀s.¬asserted occurs(heartattack,s)
∀s.asserted occurs(shoot,s) ≡ s = r(wait,r(load,S0))
asserted holds holds1(alive,S0))

(∀p e s)(holds holds1(p,s) ∧ ¬alters(e,p) ∧ ¬ab1(p,e,s) 
	⊃ holds holds1(p,r(e,s)))

¬alters(wait,loaded)
¬alters(wait,alive)
¬alters(load,alive)

If the $¬alters$ axioms are to be obtained by circumscription, it
can be a circumscription done before a specific situation is
considered, because the statements don't have a situation
parameter.
persistent p ∧ holds(p,t) ∧ (∀e)(causes(e,not p,t) ⊃ ¬occurs(e,t)) ⊃ holds(p,t+1)

persistent loaded

persistent not loaded

persistent alive

persistent not alive

holds(loaded,t) ⊃ causes(shoot,not alive,t)

causes(shoot,not loaded,t)

causes(unload,not loaded,t)

causes(load,loaded,t)

causes(e,p,t) ∧ occurs(e,t) ⊃ holds(p,t+1)

not not p = p

****
Suppose we had these sentences

holds(alive,t0)

occurs(load,t0)
¬occurs(unload,t0)
¬occurs(shoot,t0)

¬occurs(load,t0+1)
¬occurs(unload,t0+1)
¬occurs(shoot,t0+1)

¬occurs(load,t0+2)
¬occurs(unload,t0+2)
occurs(shoot,t0+2)

***
(∀p t)(holds(p,t) ∧ (∀e)(causes(e,not p,t) ⊃ ¬occurs(e,t)) ⊃ holds(p,t+1))

(∀e p t)(causes(e,p,t) ∧ occurs(e,t) ⊃ holds(p,t+1))

(∀t)causes(load,loaded,t)

(∀t)(holds(loaded,t) ⊃ causes(shoot,not alive,t))

holds(alive,0)

occurs(load,0)

occurs(wait,1)

occurs(shoot,2)

% Vladimir points out that when we minimize  causes,  we get the
% unwanted model by having  causes(wait,not loaded,1),  thereby avoiding
% causes(shoot,not alive,2).  He also remarks that he got his version
% of  causes  and  precond,  passing through a stage similar to this.
See slices[dra,val]

causes(shoot,alive,false)

precond(loaded,shoot,alive,false)

causes(load,loaded,true)

(∀p t)(holds(p,t) ∧ (∀e)(¬occurs(e,t) ∨ ¬causes(e,p,false)
 ∨ (∃q)(precond(q,e,p,false) ∧ ¬holds(q,t)) ⊃ holds(p,t+1))

(∀e p t)(causes(e,p) ∧ (∀q)(precond(q,e,f,v) ⊃ holds(q,t)) ⊃ value(f,t+1) = v))


∂29-Mar-88  1324	VAL 	re: YSP   
[In reply to message rcvd 29-Mar-88 09:37-PT.]

I agree. Here is a formulation that allows additional events. It can be used
with both discrete and continuous time. Notation: success(e,t) stands for

	occurs(e,t) ∧ ∀f[precond(f,e) ⊃ value(f,t) = true],

and affects(e,f,t) stands for

	success(e,t) ∧ ∃v causes(e,f,v).

The law of change:

success(e,t) ∧ causes(e,f,v) ⊃ ∃t'[t<t' ∧ ∀t''(t<t''≤t' ⊃ value(f,t'') = v)].

The law of inertia:

t<t' ∧ ¬∃et''[t≤t''<t' ∧ affects(e,f,t')] ⊃ value(f,t') = value(f,t).

We minimize "occurs" along with "causes" and "precond".